FDL - Nuprl Lemma : cancel_shift

Nuprl Lemma : cancel_shift

A, B:Type, opa:(A

A

A), opb:(B

B

B), f:(A

B).
Inj(A;B;f)

FunThru2op(A;B;opa;opb;f)

Cancel(B;B;opb)

Cancel(A;A;opa)

Up gen algebra 1

Definitions of Statement FunThru2op(A;B;opa;opb;f), Cancel(T;S;op)

Definitions , t T, x f y, Cancel(T;S;op), P Q, x:A. B(x), P Q, P & Q, P Q, FunThru2op(A;B;opa;opb;f), Inj(A;B;f)

Lemmas inject wf, fun thru 2op wf, cancel wf